#include <57header.h>

int main(int argc,char*argv[])
{

    printf("123 \n");

    abort();
    
    printf("456 \n");


    return 0;

}

